(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(a, f(a, f(b, f(x, y)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(x, y)))))))
f(a, f(c, f(x, y))) → f(b, f(x, y))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(z0, z1)))) → c1(F(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(z0, z1)))))), F(b, f(a, f(a, f(a, f(z0, z1))))), F(a, f(a, f(a, f(z0, z1)))), F(a, f(a, f(z0, z1))), F(a, f(z0, z1)), F(z0, z1))
F(a, f(c, f(z0, z1))) → c2(F(b, f(z0, z1)), F(z0, z1))
S tuples:
F(a, f(a, f(b, f(z0, z1)))) → c1(F(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(z0, z1)))))), F(b, f(a, f(a, f(a, f(z0, z1))))), F(a, f(a, f(a, f(z0, z1)))), F(a, f(a, f(z0, z1))), F(a, f(z0, z1)), F(z0, z1))
F(a, f(c, f(z0, z1))) → c2(F(b, f(z0, z1)), F(z0, z1))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
a,
f(
b,
f(
z0,
z1)))) →
c1(
F(
b,
f(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
z0,
z1))))))),
F(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
z0,
z1)))))),
F(
b,
f(
a,
f(
a,
f(
a,
f(
z0,
z1))))),
F(
a,
f(
a,
f(
a,
f(
z0,
z1)))),
F(
a,
f(
a,
f(
z0,
z1))),
F(
a,
f(
z0,
z1)),
F(
z0,
z1)) by
F(a, f(a, f(b, f(b, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))), F(b, f(z0, z1)))
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(c, f(z0, z1))) → c2(F(b, f(z0, z1)), F(z0, z1))
F(a, f(a, f(b, f(b, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))), F(b, f(z0, z1)))
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
S tuples:
F(a, f(c, f(z0, z1))) → c2(F(b, f(z0, z1)), F(z0, z1))
F(a, f(a, f(b, f(b, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))), F(b, f(z0, z1)))
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c2, c1, c1
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
c,
f(
z0,
z1))) →
c2(
F(
b,
f(
z0,
z1)),
F(
z0,
z1)) by
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(b, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))), F(b, f(z0, z1)))
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
S tuples:
F(a, f(a, f(b, f(b, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))), F(b, f(z0, z1)))
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c1, c2
(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
a,
f(
b,
f(
b,
f(
z0,
z1))))) →
c1(
F(
b,
f(
c,
f(
b,
f(
a,
f(
b,
f(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
z0,
z1))))))))))),
F(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1))))))),
F(
b,
f(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1)))))),
F(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1))))),
F(
a,
f(
a,
f(
b,
f(
z0,
z1)))),
F(
a,
f(
b,
f(
z0,
z1))),
F(
b,
f(
z0,
z1))) by
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
S tuples:
F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(a, f(b, f(z0, z1)))))), F(a, f(a, f(a, f(b, f(z0, z1))))), F(a, f(a, f(b, f(z0, z1)))), F(a, f(b, f(z0, z1))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c1, c2, c1
(9) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
a,
f(
b,
f(
a,
f(
b,
f(
z0,
z1)))))) →
c1(
F(
b,
f(
c,
f(
b,
f(
a,
f(
a,
f(
b,
f(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
z0,
z1)))))))))))),
F(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1)))))))),
F(
b,
f(
a,
f(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1))))))),
F(
a,
f(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1)))))),
F(
a,
f(
a,
f(
a,
f(
b,
f(
z0,
z1))))),
F(
a,
f(
a,
f(
b,
f(
z0,
z1)))),
F(
a,
f(
b,
f(
z0,
z1)))) by
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
S tuples:
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c1, c2, c1, c1
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
F(
a,
f(
a,
f(
b,
f(
c,
f(
z0,
z1))))) →
c1(
F(
b,
f(
c,
f(
b,
f(
a,
f(
a,
f(
b,
f(
z0,
z1))))))),
F(
c,
f(
b,
f(
a,
f(
a,
f(
a,
f(
c,
f(
z0,
z1))))))),
F(
b,
f(
a,
f(
a,
f(
a,
f(
c,
f(
z0,
z1)))))),
F(
a,
f(
a,
f(
a,
f(
c,
f(
z0,
z1))))),
F(
a,
f(
a,
f(
c,
f(
z0,
z1)))),
F(
a,
f(
c,
f(
z0,
z1))),
F(
c,
f(
z0,
z1))) by
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(c, f(x0, x1))))) → c1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(c, f(x0, x1))))) → c1
S tuples:
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
F(a, f(a, f(b, f(c, f(x0, x1))))) → c1
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c1, c1, c1, c1
(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
F(a, f(a, f(b, f(c, f(x0, x1))))) → c1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(a, f(a, f(b, f(z0, z1)))) → f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))
f(a, f(c, f(z0, z1))) → f(b, f(z0, z1))
Tuples:
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
S tuples:
F(a, f(a, f(b, f(x0, x1)))) → c1(F(x0, x1))
F(a, f(c, f(x0, x1))) → c2(F(x0, x1))
F(a, f(a, f(b, f(b, f(b, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))), F(b, f(b, f(z0, z1))))
F(a, f(a, f(b, f(b, f(a, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))), F(b, f(a, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(b, f(c, f(z0, z1)))))) → c1(F(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1))))))))))), F(c, f(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(b, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))), F(b, f(c, f(z0, z1))))
F(a, f(a, f(b, f(b, f(x0, x1))))) → c1(F(c, f(b, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(b, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(c, f(b, f(a, f(a, f(a, f(x0, x1))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))), F(a, f(b, f(x0, x1))))
F(a, f(a, f(b, f(a, f(b, f(b, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(b, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(b, f(z0, z1)))))), F(a, f(a, f(b, f(b, f(z0, z1))))), F(a, f(b, f(b, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(a, f(b, f(z0, z1)))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1))))))))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))))), F(a, f(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1)))))))), F(a, f(a, f(a, f(b, f(a, f(b, f(z0, z1))))))), F(a, f(a, f(b, f(a, f(b, f(z0, z1)))))), F(a, f(b, f(a, f(b, f(z0, z1))))))
F(a, f(a, f(b, f(a, f(b, f(c, f(z0, z1))))))) → c1(F(b, f(c, f(b, f(a, f(a, f(b, f(c, f(b, f(a, f(a, f(b, f(z0, z1)))))))))))), F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1)))))))), F(a, f(a, f(a, f(a, f(b, f(c, f(z0, z1))))))), F(a, f(a, f(a, f(b, f(c, f(z0, z1)))))), F(a, f(a, f(b, f(c, f(z0, z1))))), F(a, f(b, f(c, f(z0, z1)))))
F(a, f(a, f(b, f(a, f(b, f(x0, x1)))))) → c1(F(c, f(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1)))))))), F(b, f(a, f(a, f(a, f(a, f(b, f(x0, x1))))))), F(a, f(a, f(a, f(a, f(b, f(x0, x1)))))), F(a, f(a, f(a, f(b, f(x0, x1))))), F(a, f(a, f(b, f(x0, x1)))))
F(a, f(a, f(b, f(c, f(z0, z1))))) → c1(F(b, f(c, f(b, f(b, f(c, f(b, f(a, f(a, f(a, f(z0, z1)))))))))), F(c, f(b, f(a, f(a, f(a, f(c, f(z0, z1))))))), F(b, f(a, f(a, f(a, f(c, f(z0, z1)))))), F(a, f(a, f(a, f(c, f(z0, z1))))), F(a, f(a, f(c, f(z0, z1)))), F(a, f(c, f(z0, z1))), F(c, f(z0, z1)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c1, c2, c1, c1, c1
(15) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
a0() → 0
b0() → 0
c0() → 0
f0(0, 0) → 1
(16) BOUNDS(O(1), O(n^1))